\chapter*{Preface}\markboth{Preface}{Preface}
\label{intro}

This volume contains a tutorial on the \HOL{} system.  It is one of four
documents making up the documentation for \HOL:

\begin{myenumerate}
\item \LOGIC: a formal description of the higher order logic
  implemented by the \HOL{} system;
\item \TUTORIAL: a tutorial introduction to \HOL, with case studies;
\item \DESCRIPTION: a detailed user's guide for the \HOL{} system;
\item \REFERENCE: the reference manual for \HOL.
\end{myenumerate}

\noindent These four documents will be referred to by the short names (in
small slanted capitals) given above.

This document, \TUTORIAL, is intended to be the first item read by new
users of \HOL.  It provides a self-study introduction to the structure
and use of the system.  The tutorial is intended to give a `hands-on'
feel for the way \HOL{} is used, but it does not systematically
explain all the underlying principles (\DESCRIPTION{} and \LOGIC{}
explain these).  After working through \TUTORIAL\ the reader should be
capable of using \HOL\ for simple tasks, and should also be in a
position to consult the other documents.

\section*{Getting started}

Chapter~\ref{install} explains how to get and install \HOL.  Once this
is done, the potential \HOL{} user should become familiar with the
following subjects:
%
\begin{enumerate}
\item The programming meta-language \ML, and how to interact with it.
\item The formal logic supported by the \HOL{} system (higher order
  logic) and its manipulation via \ML.
\item Goal directed proof, tactics, and tacticals.
\end{enumerate}
%
Chapter~\ref{ML} introduces \ML{}.
Chapter~\ref{chap:euclid} then develops an extended example---Euclid's
proof of the infinitude of primes---to illustrate how \HOL{} is used
to prove theorems, demonstrating both the logic and proving properties of one's definitions with some high-level tactics.

Chapter~\ref{parity} features another worked example: the specification
and verification of a simple sequential parity checker.  The intention
is to accomplish two things: (i) to present another complete piece of
work with \HOL; and (ii) to give an idea of what it is like to use the
\HOL{} system for a tricky proof.  Chapter~\ref{chap:combin} is a more
extensive example: the proof of confluence for combinatory
logic.  Again, the aim is to present a complete piece of non-trivial
work.

Chapter~\ref{chap:proof-tools} gives an example of implementing a
proof tool of one's own.  This demonstrates the programmability of
\HOL: the way in which technology for solving specific problems can be
implemented on top of the underlying kernel.  With high-powered tools
to draw on, it is possible to write prototypes very quickly.

Chapter~\ref{chap:more-examples} briefly discusses some of the
examples distributed with \holn{} in the \ml{examples} directory.

%\item Chapter~\ref{tool} shows how a special purpose proof tool (a
%  conjunction normaliser) can be implemented and optimised. It
%  illustrates methods for `tuning' proof generating programs and
%  discusses trade-offs between generality and efficiency.

%\item Chapter~\ref{binomial} is a proof of the Binomial Theorem in a
%  ring.  It is a medium sized worked example whose subject matter is
%  probably more widely known than any specific piece of hardware or
%  software. The small amount of algebra and mathematical notation
%  needed to state and prove the Binomial Theorem is presented; the
%  notation is expressed in \HOL{}, and the structure of the proof is
%  outlined.

%\end{itemize}

\vspace{1cm}

\noindent \TUTORIAL{} has been kept short so that new users of \HOL{} can get
going as fast as possible. Sometimes details have been simplified. It
is recommended that as soon as a topic in \TUTORIAL\ has been
digested, the relevant parts of \DESCRIPTION\ and \REFERENCE\ be
studied.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "tutorial"
%%% End:
